Inference at * 2 2 1 2 1 1 1 1 
Iof proof for Lemma p-fun-exp-add-sq:

.....subterm..... T:t1:n

1. A : Type
2. f : A(A + Top)
3. x : A
4. m : 
5. 0 < m
6. n:. (can-apply(f^m - 1;x))  ((f^n+(m - 1)(x)) ~ (f^n(do-apply(f^m - 1;x))))
7. n : 
8. can-apply(f^m;x)
9. (n = 0)
10. (n+m = 0)
11. (n = 0)
12. (m = 0)
13. can-apply(f^m - 1;x)
14. x1 : A
15. do-apply(f^m - 1;x) = x1
  f(x1) = f^m(x) 

latex

 by ((Unfold `p-fun-exp` ( 0)) 
CollapseTHEN ((RecUnfold `primrec` 0) 
CollapseTHEN ((((if (0
C) =0 then SplitOnConclITE else SplitOnHypITE (0))) 
CollapseTHENA (Auto)) 
CollapseTHEN ((
C(Try (Trivial))) 
CollapseTHEN ((Reduce 0) 
CollapseTHEN (Fold `p-fun-exp` 0)))))) 

CoCollapseTHEN ((((if (first_bool F:b) then HypSubst' else RevHypSubst') ( -2)( 0))) 

CoCollapseTHENA (Auto)) 

latex

C1: 

C1: 16. (m = 0)
C1:   f(do-apply(f^m - 1;x)) = f o f^m - 1  (x)
C.

Definitions	Unit, P  Q, P & Q, x:A  B(x), , b, x:AB(x), SQType(T), , {x:A| B(x)} , , A  B, A, False, P  Q, {T}, s ~ t, n+m, left + right, Top, , s = t, f(a), f^n, t  T, f o g  , x:A. B(x)
Lemmas	eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, p-compose wf